(*Source vc to Low-level vc*)
structure Svc2avc2 = 
struct
  structure A = Assert
  structure E = Env4Ir
  structure V = VC
  structure I = Ir  
  structure F = Frame4Ir
  structure Err = ErrorMsg
  structure Coq = LCoqize2
  structure B = Build

(* added by lge 2006.5.14 --begin *)
  structure T = Temp
  structure P = Proof2
(* added by lge 2006.5.14 --end *)

  fun mapToAddr (id) = 0 (* cheat compiler! *)
  (* translation based on cleaned_IR, NOT AST!*)
  fun transLval' lval infunc env senv (st:A.state) = 
      let fun trans (V.Var(id)) = 
	      let val aaa = E.lookup id env
		  val (islocal, offset,types) = 
		      case aaa
		       of SOME(v) => v
			| NONE => raise Fail "no this case, compiler bug\n"
	      in if islocal 
                    then let val roff = if infunc 
					then A.Plus(A.Sel(#1 st, A.Ebp), A.IntNum(offset))
					else A.Plus(A.Sel(#1 st, A.Esp), A.IntNum(offset+8))
			 in  (fn E.Simple => (A.Sel(#2 st, roff), types, st)
			       | (E.Pointer(tp')) => (A.Sel(#2 st, roff), types, st)
			       | _ => (roff, types, st)) types
			 end
                  else (fn E.Simple => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types, st)
			 | (E.Pointer(tp')) => (A.Sel(#2 st, A.Addr(mapToAddr(id))), types, st)
			 | _ => (A.Addr(mapToAddr(id)), types, st)) types
              end
	    | trans (V.Sel(lval, exp)) = 
	      let val (subexp, types, st') = transLval' lval infunc env senv st
	      in (fn (E.Pointer(subtype)) => 
		     let val subexp' = transExp' exp infunc env senv st'
(*			 val tmptype = (fn (E.Pointer(tmptp)) => tmptp
					 | _ => raise Fail "bug") tmptype'*)
		     in (fn E.Simple => (A.Sel(#2 st', subexp'), subtype, st')
			  | (E.Pointer(tp')) => (A.Sel(#2 st', subexp'), subtype, st')
			  | _ => (subexp', subtype, st')) subtype
		     end
		   | (E.Array(_,subtype)) => 
		     let val elemSize = E.calTypeSize subtype senv
			 val index = transExp' exp infunc env senv st'
			 val offset = A.Times(index, A.IntNum(elemSize))
		     in  (fn E.Simple => (A.Sel(#2 st', A.Plus(subexp, offset)), subtype, st')
			   | (E.Pointer(tp')) => (A.Sel(#2 st', A.Plus(subexp, offset)), subtype, st')
			   | _ => (A.Plus(subexp, offset), subtype, st')) subtype
		     end
		   | (E.Struct(str)) => 
		     let val id = (fn (V.Lval(V.Var(s))) => s
				    | _ => raise Fail "bug") exp
			 val (offset, rettype) = Option.valOf(E.lookupF str id senv)
		     in (fn E.Simple => (A.Sel(#2 st', A.Plus(subexp, A.IntNum(offset))), rettype, st')
			  | (E.Pointer(tp')) => (A.Sel(#2 st', A.Plus(subexp, A.IntNum(offset))), rettype, st')
			  | _ => (A.Plus(subexp, A.IntNum(offset)), rettype, st')) rettype
		     end
		   | E.Simple => raise Fail "bug") types
	      end
	    | trans (V.Sharp(tp)) = 
	      let fun cvtType (V.Int) = E.Simple 
		    | cvtType (V.Bool) = E.Simple
		    | cvtType (V.Void) = E.Simple
		    | cvtType (V.Struct(id)) = E.Struct(id)
		    | cvtType (V.Pointer(subtype)) = E.Pointer(cvtType(subtype))
		    | cvtType (V.Array(i, subtype)) = E.Array(i, cvtType(subtype))
		  val newtp = cvtType tp
	      in (A.IntNum(1),E.Pointer(newtp), st) 
	      end
	    | trans (V.Upd(lv, e1, e2)) = (*WIP*)
	      let val (modexp', dummy_tp, st') = transLval' (V.Sel(lv, e1)) infunc env senv st
		  val modexp = (fn (A.Sel(_, ad)) => ad
				 | ad => ad) modexp'
		  val (subexp, types, dummy_st)  = transLval' lv infunc env senv st
		  val newe = transExp' e2 infunc env senv st'
		  val newst = (fn (V.Lval(V.Upd(slv, se1, se2))) => 
				  #3(transLval' (V.Upd(slv, se1, se2)) infunc env senv st')
				| _ => st') e2
		  val newst' = (#1 st, A.Upd((#2 newst), modexp, newe))
	      in (*(subexp, types, newst)*)
		 (subexp, types, newst')
	      end
	    | trans _ = raise Fail "should not happen!"
      in trans lval
      end

  and transExp' exp infunc env senv (st:A.state) = 
      let fun trans (V.IntNum(i)) = A.IntNum(i)
            | trans (V.Null) = A.Addr(0)
            | trans (V.BinopExp(e1, binop, e2)) =
              let val e1' = (transExp' e1 infunc env senv st)
                  val e2' = (transExp' e2 infunc env senv st)
              in  case binop
                   of  V.Plus => A.Plus(e1', e2')
                     | V.Minus => A.Minus(e1', e2')
                     | V.Times => A.Times(e1', e2')
                     | _ => (raise Fail "impossible"; A.Minus(e1', e2'))
              end
(*            | trans (V.Result) = A.Sel(#1 st, A.Eax)*)
(*            | trans (Ast.Prev(lval, pos)) = #1 (transLval lval infunc env senv st) *)
            | trans (V.Lval(lval)) = #1 (transLval' lval infunc env senv st)
            | trans _ = (raise Fail "impossible"; A.IntNum(0))
      in  trans exp
      end 

  fun transProp' exp infunc env senv st = 
      let fun trans V.True = A.True
	    | trans V.False = A.Not(A.True)
	    | trans (V.BinopExp(e1,binop, e2)) =
	      (case binop
                of  V.Band => 
                    A.And(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
                  | V.Bor =>
                    A.Or(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
                  | V.GT =>
                    A.Gt(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | V.GE =>
                    A.Ge(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | V.LT =>
                    A.Lt(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | V.LE =>
                    A.Le(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | V.Equ =>
                    A.Eq(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | V.NEqu =>
                    A.Ne(transExp' e1 infunc env senv st, transExp' e2 infunc env senv st)
                  | _ => (raise Fail "impossible"; A.True))
	    | trans (V.Not(e)) = A.Not(transProp' e infunc env senv st)
	    | trans (V.Imply(e1, e2)) = 
              A.Imply(transProp' e1 infunc env senv st, transProp' e2 infunc env senv st)
	    | trans (V.Forall(id, tp, e)) = 
	      trans e
	    | trans (V.Exists(id, tp, e)) = 
	      trans e
	    | trans _ = (raise Fail "not yet";A.True)
      in trans exp
      end 
  
  (* build env from ast*)
  fun bd_env ast = 
       let val env = ref (E.create())
           val senv = ref (E.creat())
           fun build (I.ExdecSkip) = ()
             | build (I.ExdecStruct(id, fieldlist, pos)) = 
               senv := B.buildSEnv id fieldlist (!senv)
             | build (I.ExdecVar(varlist, pos)) = 
               env := B.buildGEnv varlist (!env)
             | build (I.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) =
               env := B.buildFEnv (id, rettype) (!env)    
             | build (I.ExdecSeq(s1, s2, pos)) = (build s1; build s2)
           val _ = build ast
       in  (!env, !senv)
       end

  fun transet (A.Int) = P.Int
    | transet (A.Label) = P.Addr
    | transet (A.Wild) = P.Wild

  fun transe (A.IntNum(i)) = P.IntNum(i)
    | transe (A.Addr(i)) = P.AddrN(i)
    | transe (A.Plus(e1, e2)) = P.Plus(transe(e1), transe(e2))
    | transe (A.Minus(e1, e2)) = P.Minus (transe(e1), transe(e2))
    | transe (A.Times(e1, e2)) = P.Times (transe(e1), transe(e2))
    | transe (A.Eax)  = P.Eax
    | transe (A.Ebx) = P.Ebx
    | transe (A.Ecx) = P.Ecx
    | transe (A.Edx) = P.Edx
    | transe (A.Esi) = P.Esi
    | transe (A.Edi) = P.Edi
    | transe (A.Esp) = P.Esp
    | transe (A.Ebp) = P.Ebp
    | transe (A.Sel(s, e)) =
      let val (s', isrf) = transst s
          val e' = transe e 
          val lkup = if isrf
                     then P.Var("lookupR")
                     else P.Var("hr")
      in  P.App((P.App(lkup, s')), e')
      end
    | transe(_) = (raise Fail "Impossible, no CF or ZF..."; P.Eax)
  and transst (A.Rf) = (P.Var("R"), true)
    | transst (A.Hp) = (P.Var("H"), false)
    | transst (A.Upd(s, e1, e2)) = (* WIP *)
      let val (s', isrf) = transst s
          val lkup = if isrf 
                     then P.Var("updateR")
                     else P.Var("hw")
          val e1' = transe e1
          val e2' = transe e2
      in  (P.App(P.App(P.App(lkup, s'), e1'), e2'), isrf)
      end
  fun transpp (A.True) = P.True
    | transpp (A.Gt(e1, e2)) = P.Gt(transe e1, transe e2)
    | transpp (A.Ge(e1, e2)) = P.Ge(transe e1, transe e2)
    | transpp (A.Lt(e1, e2)) = P.Lt(transe e1, transe e2)
    | transpp (A.Le(e1, e2)) = P.Le(transe e1, transe e2)
    | transpp (A.Eq(e1, e2)) = P.Eq(transe e1, transe e2)
    | transpp (A.Ne(e1, e2)) = P.Ne(transe e1, transe e2)
    | transpp (A.Not(p)) = P.Not(transpp(p))
    | transpp (A.And(p1, p2)) = P.And(transpp(p1), transpp(p2))
    | transpp (A.Or(p1, p2)) = P.Or(transpp(p1), transpp(p2))
    | transpp (A.Imply(p1, p2)) = 
      let val newl = T.new_var()
          val p1' = transpp p1
          val p2' = transpp p2
      in  P.Abs((newl, P.Prop(p1')), p2')
      end
    | transpp (A.Ex((s, t), p)) = 
      let val p' = transpp p
          val t' = transet t
      in  P.Ex((s, t'), p')
      end
    | transpp (A.InDom(e, st)) =
      let val e' = transe e
          val (st', isrf) = transst st
      in  if isrf 
          then (raise Fail "InDom not in heap!"; P.True)
          else P.App(P.App(P.Var("hindom"), e'), st')  
      end
  (* added by lge 2006.5.14 --begin *)
(* give source level vc(svc), and source level vc_proof's name(label), return its proof term *)
  fun get_vc_proof svc label env senv infunc (st:A.state) =
      let val args = ref []
          val term = ref (P.Var(label))
          val _ = T.reset_var()

          fun getp (V.Forall(id, tp, exp)) st =
              let val id_inf = E.lookup id env
              in  (case id_inf 
                    of  NONE => ()
                      | _ => let val (idexp, _, _) = transLval' (V.Var(id)) infunc env senv st
                                 val idexp' = transe idexp
                             in  term := P.App ((!term), idexp')
                             end);
                  getp exp st
              end 
            | getp (V.Imply(exp1, exp2)) st =
              let val H1 = T.new_var() (*WIP*)
                  val asst = transProp' exp1 infunc env senv st
                  val pterm = transpp asst
                  val H1exp = P.Prop(pterm)
              in  args := (H1, H1exp)::(!args);
                  term := P.App (!term, P.Var(H1));
                  getp exp2 st
              end
            | getp (V.True) st = ()
            | getp (V.False) st = ()
            | getp (V.Not(e)) st = ()
            | getp (V.BinopExp(e1, V.Equ, e2)) st = ()
            | getp (V.BinopExp(e1, V.NEqu, e2)) st = ()
            | getp (V.BinopExp(e1, V.GT, e2)) st =()
            | getp (V.BinopExp(e1, V.GE, e2)) st =()
            | getp (V.BinopExp(e1, V.LT, e2)) st =()
            | getp (V.BinopExp(e1, V.LE, e2)) st =()
            | getp (V.BinopExp(e1, V.Band, e2)) st = ()
            | getp (V.BinopExp(e1, V.Bor, e2)) st =()
            | getp _ st = (raise Fail "impossible! must be prop~"; ())
          fun makefunc (arg, t) = P.Abs(arg, t)     
      in  getp svc st;
          List.foldr makefunc (!term) (!args)
      end
(* added by lge 2006.5.14 --end *)


  (* for each function *)
  fun tr_fun (fname, rettype, alist, llist) (env, senv) svclist = 
      let val frame = F.newFrame fname rettype
          val env1 = B.buildEnv alist env senv frame F.allocArgs
          val newenv = B.buildEnv llist env1 senv frame F.allocLocals
	  fun findvc ((fid, s)::r) = if fid = fname
				     then s
				     else findvc r
	    | findvc [] = V.True
	  val svc = findvc svclist
	  val avc = transProp' svc false newenv senv 
          (* modified by lge 2006.5.14 *)
          val avcp = get_vc_proof svc (fname^"_vc") newenv senv false
      in (fname, avc, avcp)
      end
  
  (* emit low-level vc*)
  fun emitVC ast svclist specs = 
      let val coqfile = TextIO.openOut((!Err.fileName)^"3.v")
	  val genv = bd_env ast
          (* modified by lge -- 2006.5.14 --begin *)
          (* clear pos field *)
          val cl_vc = List.map Irvc2vc.newmap svclist 
          (* add "foralls" to source level vcs*)
          val svclist' = Coqize.forallize cl_vc
          (* modified by lge -- 2006.5.14 --end *)
	  fun trans (I.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) = 
	      [tr_fun (id, rettype, arg, var) genv svclist']
	    | trans (I.ExdecSeq(s1, s2, pos)) = (trans s1)@(trans s2)
	    | trans _ = []
	  val avclist = trans ast
          (* modified by lge 2006.5.14 --begin *)
	  val coqtext' = String.concat(List.map (Coq.asst2coq2 specs) avclist)
          val coqtext = (Coq.coqhead()) ^ coqtext'
          (* modified by lge 2006.05.14 --end *)
      in  TextIO.output(coqfile, coqtext);
          TextIO.closeOut(coqfile)
      end

  fun emitVC' ast svclist specs= 
      let val coqfile = TextIO.openOut((!Err.fileName)^"4.v")
	  val genv = bd_env ast
          (* modified by lge -- 2006.5.14 --begin *)
          val svclist' = Coqize.forallize svclist
	  fun trans (I.ExdecFunc(id, rettype, arg, var, stm, pre, post, pos)) = 
	      [tr_fun (id, rettype, arg, var) genv svclist']
	    | trans (I.ExdecSeq(s1, s2, pos)) = (trans s1)@(trans s2)
	    | trans _ = []
          (* modified by lge -- 2006.5.14 --end *)

	  val avclist = trans ast
          (* modified by lge 2006.5.14 --begin *)
	  val coqtext' = String.concat(List.map (Coq.asst2coq2 specs) avclist)
          val coqtext = (Coq.coqhead()) ^ coqtext'
          (* modified by lge 2006.05.14 --end *)
      in  TextIO.output(coqfile, coqtext);
          TextIO.closeOut(coqfile)
      end

end
